n:, r:. 0 < r  0 < r  n 

latex

Definitions	A c B, False, A  B, , P  Q, A, P & Q, True, T, P  Q, P  Q, {T}, SQType(T), , t  T, P  Q, , x:A. B(x), Dec(P), S  T
Lemmas	le wf, qexp wf, qmul-positive, exp zero q, qmul wf, qmul one qrng, nat plus wf, exp unroll q, true wf, squash wf, decidable int equal, rationals wf, int inc rationals, qless wf, nat plus properties